| Model: | philosophers v.1 (CTMC) |
| Parameter(s) | N = 16, TIME_BOUND = 1 |
| Property: | MinExpTimeDeadlock (exp-time) |
mcsta/modest mcsta philosophers.16.jani -E TIME_BOUND=1 --props MinExpTimeDeadlock -O out.txt Minimal --unsafe --es -S Memory --no-partial-results --epsilon 0 --absolute-epsilon
| Walltime: | 37.0132360458374s |
| Return code: | 0 |
| Note(s): | The tool result '1078297345256119/100000000000000' is tagged as incorrect. The reference result is 'OrderedDict([('lower', 10.782973448921704), ('upper', 10.782973451078297)])' (approx. OrderedDict([('lower', 10.782973448921704), ('upper', 10.782973451078297)])) which means a relative error of '1.3752174878464596e-10' which is larger than the goal precision '1e-14'. |
| Relative Error: | 1.3752174878464596e-10 |
philosophers.16.jani:model: info: Philosophers16 is a CTMC model.
philosophers.16.jani: info: Need 72 bytes per state.
philosophers.16.jani: info: Explored 1331714 states for TIME_BOUND=1.0.
Peak memory usage: 1800 MB
Analysis results for philosophers.16.jani
Experiment TIME_BOUND=1.0
+ State space exploration
State size: 72 bytes
States: 1331714
Transitions: 1331714
Branches: 13774113
Rate: 100681 states/s
Time: 13.8 s
+ Property MinExpTimeDeadlock
Value: 10.78297345256119
Bounds: [10.78297345256119, 10.78297345256119]
Time: 22.6 s
+ Precomputations
Min. prob. 0 states: 0
Time for min. prob. 0 states: 0.6 s
Min. prob. 1 states: 1331714
Time for min. prob. 1 states: 0.2 s
+ Essential states
Iterations: 1
Essential states: 1331715
Transitions: 1331715
Branches: 13774114
Time: 0.9 s
+ Value iteration
Final error: 0
Iterations: 185
Time: 20.9 s
Exported results to file "/out.txt".
The Modest Toolset (www.modestchecker.net), version v3.1.42-gb5e9d523c.